Termination w.r.t. Q proof of TRS/D3301.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

\(x, x) → e
/(x, x) → e
.(e, x) → x
.(x, e) → x
\(e, x) → x
/(x, e) → x
.(x, \(x, y)) → y
.(/(y, x), x) → y
\(x, .(x, y)) → y
/(.(y, x), x) → y
/(x, \(y, x)) → y
\(/(x, y), x) → y

Q is empty.

↳ QTRS

  ↳ DirectTerminationProof

Q restricted rewrite system:
The TRS R consists of the following rules:

\(x, x) → e
/(x, x) → e
.(e, x) → x
.(x, e) → x
\(e, x) → x
/(x, e) → x
.(x, \(x, y)) → y
.(/(y, x), x) → y
\(x, .(x, y)) → y
/(.(y, x), x) → y
/(x, \(y, x)) → y
\(/(x, y), x) → y

Q is empty.

We use [23] with the following order to prove termination.

Lexicographic path order with status [19].
Quasi-Precedence:

\₂ > e
/₂ > e

Status:

trivial